YES 0.483 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule Monad
  ((liftM5 :: (b  ->  f  ->  e  ->  c  ->  d  ->  a)  ->  IO b  ->  IO f  ->  IO e  ->  IO c  ->  IO d  ->  IO a) :: (b  ->  f  ->  e  ->  c  ->  d  ->  a)  ->  IO b  ->  IO f  ->  IO e  ->  IO c  ->  IO d  ->  IO a)

module Monad where
  import qualified Maybe
import qualified Prelude
  liftM5 :: Monad f => (d  ->  c  ->  g  ->  b  ->  a  ->  e)  ->  f d  ->  f c  ->  f g  ->  f b  ->  f a  ->  f e
liftM5 f m1 m2 m3 m4 m5 = m1 >>= (\x1 ->m2 >>= (\x2 ->m3 >>= (\x3 ->m4 >>= (\x4 ->m5 >>= (\x5 ->return (f x1 x2 x3 x4 x5))))))


module Maybe where
  import qualified Monad
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\x5→return (f x1 x2 x3 x4 x5)

is transformed to
liftM50 f x1 x2 x3 x4 x5 = return (f x1 x2 x3 x4 x5)

The following Lambda expression
\x4→m5 >>= liftM50 f x1 x2 x3 x4

is transformed to
liftM51 m5 f x1 x2 x3 x4 = m5 >>= liftM50 f x1 x2 x3 x4

The following Lambda expression
\x3→m4 >>= liftM51 m5 f x1 x2 x3

is transformed to
liftM52 m4 m5 f x1 x2 x3 = m4 >>= liftM51 m5 f x1 x2 x3

The following Lambda expression
\x2→m3 >>= liftM52 m4 m5 f x1 x2

is transformed to
liftM53 m3 m4 m5 f x1 x2 = m3 >>= liftM52 m4 m5 f x1 x2

The following Lambda expression
\x1→m2 >>= liftM53 m3 m4 m5 f x1

is transformed to
liftM54 m2 m3 m4 m5 f x1 = m2 >>= liftM53 m3 m4 m5 f x1



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR

mainModule Monad
  ((liftM5 :: (d  ->  e  ->  a  ->  f  ->  c  ->  b)  ->  IO d  ->  IO e  ->  IO a  ->  IO f  ->  IO c  ->  IO b) :: (d  ->  e  ->  a  ->  f  ->  c  ->  b)  ->  IO d  ->  IO e  ->  IO a  ->  IO f  ->  IO c  ->  IO b)

module Maybe where
  import qualified Monad
import qualified Prelude

module Monad where
  import qualified Maybe
import qualified Prelude
  liftM5 :: Monad f => (d  ->  b  ->  c  ->  e  ->  g  ->  a)  ->  f d  ->  f b  ->  f c  ->  f e  ->  f g  ->  f a
liftM5 f m1 m2 m3 m4 m5 = m1 >>= liftM54 m2 m3 m4 m5 f

  
liftM50 f x1 x2 x3 x4 x5 = return (f x1 x2 x3 x4 x5)

  
liftM51 m5 f x1 x2 x3 x4 = m5 >>= liftM50 f x1 x2 x3 x4

  
liftM52 m4 m5 f x1 x2 x3 = m4 >>= liftM51 m5 f x1 x2 x3

  
liftM53 m3 m4 m5 f x1 x2 = m3 >>= liftM52 m4 m5 f x1 x2

  
liftM54 m2 m3 m4 m5 f x1 = m2 >>= liftM53 m3 m4 m5 f x1



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR

mainModule Monad
  ((liftM5 :: (b  ->  c  ->  e  ->  f  ->  d  ->  a)  ->  IO b  ->  IO c  ->  IO e  ->  IO f  ->  IO d  ->  IO a) :: (b  ->  c  ->  e  ->  f  ->  d  ->  a)  ->  IO b  ->  IO c  ->  IO e  ->  IO f  ->  IO d  ->  IO a)

module Monad where
  import qualified Maybe
import qualified Prelude
  liftM5 :: Monad b => (d  ->  c  ->  a  ->  g  ->  f  ->  e)  ->  b d  ->  b c  ->  b a  ->  b g  ->  b f  ->  b e
liftM5 f m1 m2 m3 m4 m5 = m1 >>= liftM54 m2 m3 m4 m5 f

  
liftM50 f x1 x2 x3 x4 x5 = return (f x1 x2 x3 x4 x5)

  
liftM51 m5 f x1 x2 x3 x4 = m5 >>= liftM50 f x1 x2 x3 x4

  
liftM52 m4 m5 f x1 x2 x3 = m4 >>= liftM51 m5 f x1 x2 x3

  
liftM53 m3 m4 m5 f x1 x2 = m3 >>= liftM52 m4 m5 f x1 x2

  
liftM54 m2 m3 m4 m5 f x1 = m2 >>= liftM53 m3 m4 m5 f x1


module Maybe where
  import qualified Monad
import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow

mainModule Monad
  (liftM5 :: (c  ->  d  ->  f  ->  e  ->  a  ->  b)  ->  IO c  ->  IO d  ->  IO f  ->  IO e  ->  IO a  ->  IO b)

module Maybe where
  import qualified Monad
import qualified Prelude

module Monad where
  import qualified Maybe
import qualified Prelude
  liftM5 :: Monad d => (a  ->  c  ->  g  ->  b  ->  e  ->  f)  ->  d a  ->  d c  ->  d g  ->  d b  ->  d e  ->  d f
liftM5 f m1 m2 m3 m4 m5 = m1 >>= liftM54 m2 m3 m4 m5 f

  
liftM50 f x1 x2 x3 x4 x5 = return (f x1 x2 x3 x4 x5)

  
liftM51 m5 f x1 x2 x3 x4 = m5 >>= liftM50 f x1 x2 x3 x4

  
liftM52 m4 m5 f x1 x2 x3 = m4 >>= liftM51 m5 f x1 x2 x3

  
liftM53 m3 m4 m5 f x1 x2 = m3 >>= liftM52 m4 m5 f x1 x2

  
liftM54 m2 m3 m4 m5 f x1 = m2 >>= liftM53 m3 m4 m5 f x1



Haskell To QDPs